-----------------------------
MODULE service_manager
-----------------------------

EXTENDS capability_system, memory_manager, TLC, FiniteSets

(*
 * ZENrs Service Manager 形式化模型
 *
 * 此模块形式化描述了 safe_services/src/lib.rs 中的 ServiceManager 结构体行为
 * 验证其服务初始化顺序、资源获取和释放的安全性
 *)

(* 服务类型定义 *)
ServiceType == {"MemoryService", "ProcessService", "FileSystemService", 
                "NetworkService", "GraphicsService", "VulkanService", 
                "SkiaService", "WaylandService", "IPCService", 
                "DriverService", "KuiklyUIService", "GraphicsSubsystem", 
                "ShellService"}

(* 服务状态定义 *)
ServiceState == [
    name: ServiceType,
    initialized: Bool,
    started: Bool,
    requiredCapabilities: Set(CapabilityId)
]

(* 系统状态变量 *)
VARIABLES
    \* 服务管理器状态
    serviceManagerState,
    
    \* 各服务状态
    services,
    
    \* 能力系统状态
    capabilities,
    
    \* 内存管理状态
    memoryMap

(* 常量定义 *)
InitProcessId == 1
MemoryCapabilityId == 100
CPUCapabilityId == 101

(* 服务依赖关系定义 *)
ServiceDependencies == [
    "MemoryService" |-> {},
    "ProcessService" |-> {"MemoryService"},
    "FileSystemService" |-> {"MemoryService"},
    "NetworkService" |-> {"MemoryService"},
    "GraphicsService" |-> {"MemoryService"},
    "VulkanService" |-> {"GraphicsService", "MemoryService"},
    "SkiaService" |-> {"GraphicsService", "VulkanService", "MemoryService"},
    "WaylandService" |-> {"GraphicsService", "MemoryService"},
    "IPCService" |-> {"MemoryService"},
    "DriverService" |-> {"MemoryService"},
    "KuiklyUIService" |-> {"MemoryService"},
    "GraphicsSubsystem" |-> {"GraphicsService", "VulkanService", "SkiaService", "WaylandService", "KuiklyUIService", "MemoryService"},
    "ShellService" |-> {"MemoryService", "ProcessService"}
]

(* 初始状态 *)
Init ==
    /\ serviceManagerState = "Initialized"
    /\ services = [
        "MemoryService" |-> [
            name |-> "MemoryService",
            initialized |-> FALSE,
            started |-> FALSE,
            requiredCapabilities |-> {MemoryCapabilityId}
        ],
        "ProcessService" |-> [
            name |-> "ProcessService",
            initialized |-> FALSE,
            started |-> FALSE,
            requiredCapabilities |-> {CPUCapabilityId, MemoryCapabilityId}
        ],
        "FileSystemService" |-> [
            name |-> "FileSystemService",
            initialized |-> FALSE,
            started |-> FALSE,
            requiredCapabilities |-> {MemoryCapabilityId}
        ],
        "NetworkService" |-> [
            name |-> "NetworkService",
            initialized |-> FALSE,
            started |-> FALSE,
            requiredCapabilities |-> {MemoryCapabilityId}
        ],
        "GraphicsService" |-> [
            name |-> "GraphicsService",
            initialized |-> FALSE,
            started |-> FALSE,
            requiredCapabilities |-> {MemoryCapabilityId}
        ],
        "VulkanService" |-> [
            name |-> "VulkanService",
            initialized |-> FALSE,
            started |-> FALSE,
            requiredCapabilities |-> {MemoryCapabilityId}
        ],
        "SkiaService" |-> [
            name |-> "SkiaService",
            initialized |-> FALSE,
            started |-> FALSE,
            requiredCapabilities |-> {MemoryCapabilityId}
        ],
        "WaylandService" |-> [
            name |-> "WaylandService",
            initialized |-> FALSE,
            started |-> FALSE,
            requiredCapabilities |-> {MemoryCapabilityId}
        ],
        "IPCService" |-> [
            name |-> "IPCService",
            initialized |-> FALSE,
            started |-> FALSE,
            requiredCapabilities |-> {MemoryCapabilityId}
        ],
        "DriverService" |-> [
            name |-> "DriverService",
            initialized |-> FALSE,
            started |-> FALSE,
            requiredCapabilities |-> {MemoryCapabilityId}
        ],
        "KuiklyUIService" |-> [
            name |-> "KuiklyUIService",
            initialized |-> FALSE,
            started |-> FALSE,
            requiredCapabilities |-> {MemoryCapabilityId}
        ],
        "GraphicsSubsystem" |-> [
            name |-> "GraphicsSubsystem",
            initialized |-> FALSE,
            started |-> FALSE,
            requiredCapabilities |-> {MemoryCapabilityId}
        ],
        "ShellService" |-> [
            name |-> "ShellService",
            initialized |-> FALSE,
            started |-> FALSE,
            requiredCapabilities |-> {MemoryCapabilityId}
        ]
    ]
    /\ capabilities = [
        MemoryCapabilityId |-> [id |-> MemoryCapabilityId, acquired |-> FALSE],
        CPUCapabilityId |-> [id |-> CPUCapabilityId, acquired |-> FALSE]
    ]
    /\ memoryMap = empty

(* 初始化服务 *)
InitService(serviceName) ==
    /\ serviceName \in ServiceType
    /\ ~services[serviceName].initialized
    /\ LET 
        deps = ServiceDependencies[serviceName]
        depsInitialized = \A dep \in deps: services[dep].initialized
        reqCaps = services[serviceName].requiredCapabilities
        capsAvailable = \A capId \in reqCaps: 
            capId \in DOMAIN capabilities /\ ~capabilities[capId].acquired
    IN 
        /\ depsInitialized
        /\ capsAvailable
        /\ services' = [services EXCEPT ![serviceName].initialized = TRUE]
        /\ UNCHANGED <<serviceManagerState, capabilities, memoryMap>>

(* 启动服务 *)
StartService(serviceName) ==
    /\ serviceName \in ServiceType
    /\ services[serviceName].initialized
    /\ ~services[serviceName].started
    /\ LET reqCaps = services[serviceName].requiredCapabilities
    IN 
        /\ \A capId \in reqCaps: 
            capabilities[capId].acquired
        /\ services' = [services EXCEPT ![serviceName].started = TRUE]
        /\ UNCHANGED <<serviceManagerState, capabilities, memoryMap>>

(* 获取能力 *)
AcquireCapability(capId) ==
    /\ capId \in DOMAIN capabilities
    /\ ~capabilities[capId].acquired
    /\ capabilities' = [capabilities EXCEPT ![capId].acquired = TRUE]
    /\ UNCHANGED <<serviceManagerState, services, memoryMap>>

(* 释放能力 *)
ReleaseCapability(capId) ==
    /\ capId \in DOMAIN capabilities
    /\ capabilities[capId].acquired
    /\ LET servicesUsingCap = {s \in ServiceType: 
        capId \in services[s].requiredCapabilities /\ services[s].started}
    IN 
        /\ servicesUsingCap = {}
        /\ capabilities' = [capabilities EXCEPT ![capId].acquired = FALSE]
        /\ UNCHANGED <<serviceManagerState, services, memoryMap>>

(* 停止服务 *)
StopService(serviceName) ==
    /\ serviceName \in ServiceType
    /\ services[serviceName].started
    /\ LET 
        dependentServices = {s \in ServiceType: 
            serviceName \in ServiceDependencies[s] /\ services[s].started}
    IN 
        /\ dependentServices = {}
        /\ services' = [services EXCEPT ![serviceName].started = FALSE]
        /\ UNCHANGED <<serviceManagerState, capabilities, memoryMap>>

(* 下一个状态 *)
Next ==
    \E serviceName \in ServiceType:
        InitService(serviceName) \/
        StartService(serviceName) \/
        StopService(serviceName)
    \/
    \E capId \in DOMAIN capabilities:
        AcquireCapability(capId) \/
        ReleaseCapability(capId)

(* 安全属性定义 *)

(* 服务初始化顺序正确性：服务只能在其依赖服务初始化后才能初始化 *)
ServiceInitOrderCorrectness == 
    \A serviceName \in ServiceType:
        services[serviceName].initialized => 
        (\A dep \in ServiceDependencies[serviceName]: 
            services[dep].initialized)

(* 服务启动顺序正确性：服务只能在其依赖服务启动后才能启动 *)
ServiceStartOrderCorrectness == 
    \A serviceName \in ServiceType:
        services[serviceName].started => 
        (services[serviceName].initialized /\
         \A dep \in ServiceDependencies[serviceName]: 
            services[dep].started)

(* 能力使用安全性：服务只能在获取所需能力后才能启动 *)
CapabilityUsageSafety == 
    \A serviceName \in ServiceType:
        services[serviceName].started => 
        (\A capId \in services[serviceName].requiredCapabilities: 
            capabilities[capId].acquired)

(* 能力释放安全性：只有当没有服务使用能力时才能释放能力 *)
CapabilityReleaseSafety == 
    \A capId \in DOMAIN capabilities:
        ~capabilities[capId].acquired => 
        (\A serviceName \in ServiceType: 
            (capId \in services[serviceName].requiredCapabilities => 
             ~services[serviceName].started))

(* 服务停止顺序正确性：服务只能在依赖它的服务停止后才能停止 *)
ServiceStopOrderCorrectness == 
    \A serviceName \in ServiceType:
        ~services[serviceName].started => 
        (\A s \in ServiceType: 
            (serviceName \in ServiceDependencies[s] => 
             ~services[s].started))

(* 内存服务优先性：内存服务必须首先初始化和启动 *)
MemoryServicePriority == 
    services["MemoryService"].initialized => 
    (\A s \in ServiceType \ {"MemoryService"}: 
        ~services[s].initialized => 
        services["MemoryService"].initialized)

(* 验证配置 *)

(* 模型检查的不变式 *)
Spec == Init /\ [][Next]_<<serviceManagerState, services, capabilities, memoryMap>>

(* 要验证的不变式 *)
Inv == 
    ServiceInitOrderCorrectness /\
    ServiceStartOrderCorrectness /\
    CapabilityUsageSafety /\
    CapabilityReleaseSafety /\
    ServiceStopOrderCorrectness /\
    MemoryServicePriority

(* TLC配置 *)

(* 限制状态空间大小 *)
CONSTANTS MaxServices = 13, MaxCapabilities = 2

(* 模型检查 *)
Check == TLC!Spec \/\ TLC!Inv

(*
运行此模型：
1. 使用TLA+工具box打开此文件
2. 配置TLC模型检查器，设置不变式为Inv
3. 运行模型检查

预期结果：
- 所有不变式应成立
- 没有违反服务初始化和启动顺序的情况
- 没有能力使用安全问题
*)